<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>Stand-alone seL4 builds | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/projects/">
              <span property="name"><b>Projects</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/projects/buildsystem/">
              <span property="name"><b>System configuration and building</b></span>
            </a>
            <meta property="position" content="3" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">Stand-alone seL4 builds</span>
            <meta property="position" content="4" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    


<div class="sidebar">















    <ul class="nav nav-sidebar">
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4/">seL4</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/l4v/">L4.verified</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/camkes/">CAmkES</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/capdl/">CapDL</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/elfloader/">Elfloader</a>
        </li>
  
    
    

    
        <li class="active">
            <a class="" href="/projects/buildsystem/">seL4 Buildsystem</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/user_libs/">user_libs</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4runtime/">The seL4 run-time</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4webserver/">seL4webserver</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4-tutorials/">seL4 tutorials</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4bench/">sel4bench</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4test/">seL4Test</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/virtualization/">Virtualization</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/camkes-vm/">camkes-vm</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/dockerfiles/">Dockerfiles</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/docsite/">seL4 Documentation website</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4_tools/">seL4_tools</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/microkit/">Microkit</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/hardware_hacks/">Hardware Hacks</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/rust/">Rust</a>
        </li>
  
    </ul>


</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">
    <h1 id="stand-alone-sel4-builds">Stand-alone seL4 builds</h1>

<!--excerpt-->

<p>This page contains documentation for building the seL4 kernel standalone — without a userlevel or any loaders that run before the kernel. This is typically used for verification or where a project wants to fully control userlevel and prekernel initialisation. We only maintain verification configurations for kernel only builds.  This page assumes familiarity with using the seL4 project build system and builds upon the previous documentation.</p>

<!--excerpt-->

<p><em>Note: it is assumed that you know what to do with a generated kernel.elf binary.  For an explanation see at the bottom of the page.</em></p>

<h2 id="building-a-kernel-standalone">Building a kernel standalone</h2>

<h3 id="initialising-build-directory-with-existing-configuration">Initialising build directory with existing configuration</h3>

<p>Building the kernel standalone requires initialising a cmake build directory using the seL4 repo as the root CMake project:</p>
<pre><code class="language-none">├── seL4/
│   └── CMakeLists.txt
├── build/ # Current directory
</code></pre>

<p>The build directory is initialised as follows:</p>
<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code>cmake <span class="nt">-DCROSS_COMPILER_PREFIX</span><span class="o">=</span> <span class="nt">-DCMAKE_TOOLCHAIN_FILE</span><span class="o">=</span>../seL4/gcc.cmake <span class="nt">-G</span> Ninja <span class="nt">-C</span> ../seL4/configs/X64_verified.cmake ../seL4/
</code></pre></div></div>
<p>We use the X64_verified.cmake file for configuration values.</p>

<p>To find available verification configurations:</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">ls</span> ../seL4/configs/<span class="k">*</span>.cmake
<span class="c"># ../seL4/configs/ARM_HYP_verified.cmake  ../seL4/configs/X64_verified.cmake</span>
<span class="c"># ../seL4/configs/ARM_verified.cmake</span>
</code></pre></div></div>

<p>A typical verification configuration (<code class="language-plaintext highlighter-rouge">cat ../seL4/configs/X64_verified.cmake</code>):</p>

<div class="language-cmake highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c1">#!/usr/bin/env -S cmake -P</span>
<span class="c1">#</span>
<span class="c1"># Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)</span>
<span class="c1">#</span>
<span class="c1"># SPDX-License-Identifier: GPL-2.0-only</span>
<span class="c1">#</span>

<span class="c1"># If this file is executed then build the kernel.elf and kernel_all_pp.c file</span>
<span class="nb">include</span><span class="p">(</span><span class="si">${</span><span class="nv">CMAKE_CURRENT_LIST_DIR</span><span class="si">}</span>/../tools/helpers.cmake<span class="p">)</span>
<span class="nf">cmake_script_build_kernel</span><span class="p">()</span>

<span class="nb">set</span><span class="p">(</span>KernelPlatform <span class="s2">"pc99"</span> CACHE STRING <span class="s2">""</span><span class="p">)</span>
<span class="nb">set</span><span class="p">(</span>KernelSel4Arch <span class="s2">"x86_64"</span> CACHE STRING <span class="s2">""</span><span class="p">)</span>
<span class="nb">set</span><span class="p">(</span>KernelVerificationBuild ON CACHE BOOL <span class="s2">""</span><span class="p">)</span>
<span class="nb">set</span><span class="p">(</span>KernelMaxNumNodes <span class="s2">"1"</span> CACHE STRING <span class="s2">""</span><span class="p">)</span>
<span class="nb">set</span><span class="p">(</span>KernelOptimisation <span class="s2">"-O2"</span> CACHE STRING <span class="s2">""</span><span class="p">)</span>
<span class="nb">set</span><span class="p">(</span>KernelRetypeFanOutLimit <span class="s2">"256"</span> CACHE STRING <span class="s2">""</span><span class="p">)</span>
<span class="nb">set</span><span class="p">(</span>KernelBenchmarks <span class="s2">"none"</span> CACHE STRING <span class="s2">""</span><span class="p">)</span>
<span class="nb">set</span><span class="p">(</span>KernelDangerousCodeInjection OFF CACHE BOOL <span class="s2">""</span><span class="p">)</span>
<span class="nb">set</span><span class="p">(</span>KernelFastpath ON CACHE BOOL <span class="s2">""</span><span class="p">)</span>
<span class="nb">set</span><span class="p">(</span>KernelPrinting OFF CACHE BOOL <span class="s2">""</span><span class="p">)</span>
<span class="nb">set</span><span class="p">(</span>KernelNumDomains 16 CACHE STRING <span class="s2">""</span><span class="p">)</span>
<span class="nb">set</span><span class="p">(</span>KernelMaxNumBootinfoUntypedCap 166 CACHE STRING <span class="s2">""</span><span class="p">)</span>
<span class="nb">set</span><span class="p">(</span>KernelRootCNodeSizeBits 19 CACHE STRING <span class="s2">""</span><span class="p">)</span>
<span class="nb">set</span><span class="p">(</span>KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING <span class="s2">""</span><span class="p">)</span>
<span class="nb">set</span><span class="p">(</span>KernelFSGSBase <span class="s2">"inst"</span> CACHE STRING <span class="s2">""</span><span class="p">)</span>
</code></pre></div></div>

<p>At this point you could use <code class="language-plaintext highlighter-rouge">ccmake ../seL4</code> to browse the configuration.</p>

<h3 id="building-the-kernel-target">Building the kernel target</h3>

<p>The kernel target needs to be specified to <code class="language-plaintext highlighter-rouge">ninja</code> otherwise it won’t be built.</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code>ninja kernel.elf
</code></pre></div></div>

<p>Looking in the build directory:</p>
<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">ls</span>
<span class="c"># autoconf                 gen_config       kernel_all_pp.c                      kernel.elf</span>
<span class="c"># build.ninja              generated        kernel_all_pp_prune.c                linker.lds_pp</span>
<span class="c"># circular_includes_valid  generated_prune  kernel_all_pp_prune_wrapper_temp.c   linker_ld_wrapper_temp.c</span>
<span class="c"># CMakeCache.txt           gen_headers      kernel_bf_gen_target_111_pbf_temp.c  rules.ninja</span>
<span class="c"># CMakeFiles               kernel_all.c     kernel_bf_gen_target_11_pbf_temp.c</span>
<span class="c"># cmake_install.cmake      kernel_all.i     kernel_bf_gen_target_1_pbf_temp.c</span>
</code></pre></div></div>

<p>The kernel.elf can now be used in other build environments.</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code>file kernel.elf
<span class="c"># kernel.elf: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), statically linked, not stripped</span>
</code></pre></div></div>

<h2 id="installing">Installing</h2>

<p>The build directory contains many more artefacts than needed to use a standalone kernel build.</p>

<p>If you have used <code class="language-plaintext highlighter-rouge">-DCMAKE_INSTALL_PREFIX=&lt;install dir&gt;</code> when configuring CMake and then run <code class="language-plaintext highlighter-rouge">cmake --install &lt;build dir&gt;</code>,
you can have all the install artefacts placed in <code class="language-plaintext highlighter-rouge">&lt;install dir&gt;</code>. The directory structure is the following:</p>

<pre><code class="language-none">├── bin/
│   └── kernel.elf
├── libsel4/
|   ├── include/
|   |   └── ...
|   |   └── kernel/
|   |       └── ...
|   |       └── gen_config.json
|   └── src/
├── support/
|   └── kernel.dtb
|   └── platform_gen.json
|   └── platform_gen.yaml
</code></pre>

<p>Note that the contents of the <code class="language-plaintext highlighter-rouge">support/</code> directory may differ depending on the target architecture.</p>

<h2 id="why-use-stand-alone-build">Why use stand alone build?</h2>

<p>It is non-trivial to take a standalone kernel.elf and use it in another build environment.  This is because the system configuration is not exported with the kernel.elf and so a different build environment will need to know exactly how the kernel was configured so that bootloaders and userlevel applications can be configured in a compatible way.  Using the CMake scripts provided in seL4_tools and importing the kernel into an existing CMake project hierarchy will ensure that the system configuration is properly shared with other parts of the project.</p>

<p>However sometimes a standalone build is required when the kernel is being used in a different environment that doesn’t use a CMake based build system.  One example of this is the verification project, L4V, that uses the stand alone build to produce the source and binary artifacts that the verification is performed on.</p>

<p>Other use cases include projects that want to build a non-C root task, or projects that are already sophisticated enough to manage the different configuration settings that the kernel requires.  In these scenarios, it would be expected that these projects provide their own Configuration.cmake files that have correct configurations.</p>

  </div>







  
  
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
  
    <ul class="section-nav">
    	<h2> seL4 Buildsystem </h2> 
        <li>
          
          <a style="" class="" href="/projects/buildsystem/">
            Documentation homepage
          </a>
        </li>

















    
        <h3>Repositories</h3>
    
        <li>
          <a class="" href="https://github.com/sel4/sel4">
            sel4
          </a>
        </li>

    
        <li>
          <a class="" href="https://github.com/sel4/sel4_tools">
            sel4_tools
          </a>
        </li>









  







    
        <h3>Recent Updates</h3>
    
        <li>
          <a style="" href="/updates/buildsystem/11.0.x.html">
            seL4 11.0.x-compatible
          </a>
        </li>

    </ul>

</div>


</div>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Tue Jul 2 12:58:52 2024 +1000 d66da26e94
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/projects/buildsystem/standalone.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/projects/buildsystem/standalone.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
